Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    primes  → sieve(from(s(s(0))))
2:    from(X)  → cons(X,from(s(X)))
3:    head(cons(X,Y))  → X
4:    tail(cons(X,Y))  → Y
5:    if(true,X,Y)  → X
6:    if(false,X,Y)  → Y
7:    filter(s(s(X)),cons(Y,Z))  → if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
8:    sieve(cons(X,Y))  → cons(X,filter(X,sieve(Y)))
There are 9 dependency pairs:
9:    PRIMES  → SIEVE(from(s(s(0))))
10:    PRIMES  → FROM(s(s(0)))
11:    FROM(X)  → FROM(s(X))
12:    FILTER(s(s(X)),cons(Y,Z))  → IF(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
13:    FILTER(s(s(X)),cons(Y,Z))  → FILTER(s(s(X)),Z)
14:    FILTER(s(s(X)),cons(Y,Z))  → FILTER(X,sieve(Y))
15:    FILTER(s(s(X)),cons(Y,Z))  → SIEVE(Y)
16:    SIEVE(cons(X,Y))  → FILTER(X,sieve(Y))
17:    SIEVE(cons(X,Y))  → SIEVE(Y)
The approximated dependency graph contains 2 SCCs: {11} and {13-17}.
Tyrolean Termination Tool  (0.46 seconds)   ---  May 3, 2006